Section: New Results

Software specification and verification

Proved time complexity bounds for program components

Participants : Sylvain Dailler, François Pottier.

During a six-month master internship (M2), Sylvain Dailler extended Arthur Charguéraud's CFML tool with a notion of “time credit”. This allows CFML to be used to prove not only that an algorithm (or a data structure, or a library) is correct, but also that it meets a desired worst-case asymptotic complexity bound. Because CFML is hosted within Coq, these proofs are machine-checked. Sylvain Dailler was able to establish the functional correctness and the time complexity of a library that implements “bags” as circular doubly-linked lists [35] .

Hybrid contract checking via symbolic simplification

Participant : Na Xu.

Program errors are hard to detect or prove absent. Allowing programmers to write formal and precise specifications, especially in the form of contracts, is one popular approach to program verification and error discovery. Na Xu formalized and implemented a hybrid contract checker for a subset of OCaml. The key technique is the use of symbolic simplification, which makes integrating static and dynamic contract checking easy and effective. This technique statically verifies that a function satisfies its contract or blames the function violating the contract. When a contract satisfaction is undecidable, it leaves residual code for dynamic contract checking. A paper describing this result will be presented at the PEPM'2012 conference [30] . A technical report version is also available [34] .

Tools for TLA+

Participants : Damien Doligez, Leslie Lamport [Microsoft Research] , Stephan Merz [EPI VeriDis] , Denis Cousineau [Microsoft Research-INRIA Joint Centre] , Markus Kuppe [Microsoft Research-INRIA Joint Centre] , Hernán Vanzetto [Microsoft Research-INRIA Joint Centre] .

Damien Doligez is head of the “Tools for Proofs” team in the Microsoft-INRIA Joint Centre. The aim of this team is to extend the TLA+ language with a formal language for hierarchical proofs, formalizing the ideas in  [45] , and to build tools for writing TLA+ specifications and mechanically checking the corresponding formal proofs.

This year, the TLA+ project prepared the release of the third version of the TLA+ tools: the GUI-based TLA Toolbox and the TLA+ Proof System, an environment for writing and checking TLA+ proofs. This new release will add many improvements in terms of efficiency, notably with a system of fingerprints to support incremental development of proofs. It will also bring support for new back-ends based on SMT provers (CVC3, Z3, Yices, VeriT). This extends the range of proof obligations that the system can discharge automatically.

Web site: http://tlaplus.net/ .

The Zenon automatic theorem prover

Participant : Damien Doligez.

Damien Doligez continued the development of Zenon, a tableau-based prover for first-order logic with equality and theory-specific extensions. This year, a refactoring of the prover's architecture was started.